$\forall$$A$, $B$:Realizer. R{-}interface{-}compat($A$;$B$) $\in$ Prop